Seems like the store and heap would fit better in a State monad

Agreed this would be cleaner. However, the explicit state threading is currently used directly by the fuel monotonicity proof in LaurelDenoteMono.lean, which pattern-matches on the (Outcome × LaurelStore × LaurelHeap) tuples. If that's fine with you I'll file this as a follow-up refactor — we'd need to verify the monotonicity proof still works through the monad abstraction.

What's denotational about this? An AI summary of "denotational semantics" is "Denotational semantics defines programming language meaning by mapping syntactic constructs directly to mathematical objects (denotations), rather than simulating execution steps", which seems opposite of what this implementation does. The wiki on denotational semantics also doesn't relate to this type of semantics.

Fair point. This is a fuel-based recursive interpreter, not denotational semantics in the classical sense (mapping syntax to mathematical domains). It is however very close to how we usually define a denotational semantics, e.g. in https://www.cs.utexas.edu/~bornholt/courses/cs345h-22au/lectures/2-interpreters/, as it defines the meaning (denotation) of an AST construct as a function mapping a state to the outcome value.

For simplicity and clarity though, I renamed throughout:

• LaurelDenote.lean → LaurelInterpreter.lean
• LaurelDenoteMono.lean → LaurelInterpreterMono.lean
• All doc comments updated from "denotational" to "interpreter"
• Function names (denoteStmt, denoteBlock, denoteArgs) renamed to interpStmt, interpBlock, interpArgs
• Test files renamed accordingly

If we want to use the semantic definition to verify that the compilation correctly maintains the mapping of source locations, then the Outcome here needs to be more detailed when errors occur, for example by containing a DiagnosticModel.

Agree. This would be IMO the next step in the definition of the semantics: a more fine grained handling of the non-normal outcome. If that's fine with you, I would like to defer it to a follow-up addition. I added a TODO comment and will file an issue to track this.

Runtime compilation might erase assertions and assumptions, and to do that safely their bodies should not have side-effects. The semantics here should check that if the heap/store changes, none is returned.

Agreed in principle. The interpreter already discards the post-condition store/heap and returns the originals, so side effects in assert/assume conditions are invisible to subsequent code. However, we cannot detect impure conditions at runtime because LaurelStore and LaurelHeap are function types (String ? Option LaurelValue and Nat ? Option (...)) which have no BEq or DecidableEq instance in Lean. There is no way to compare two closures for equality. The purity requirement must be enforced statically (e.g., by a well-formedness check on the AST before interpretation) rather than dynamically. Added documentation clarifying this design constraint.

After moving the heap and store into a State monad, do notation can be used for all these cases to make them much nicer to read.

.PrimitiveOp op args => do
  let vals <- denoteArgs δ π fuel args
  evalPrimOp op vals

Agreed, this would be much cleaner with do-notation. Will address together with the State monad refactor (see comment 1).

It seems you're leaving the meaning of quantifiers unspecified. How about you enable δ to return a List of all possible values of a particular type? Then you can use the fuel to iterate over these values and check the property.

Interesting idea. The current δ callback was designed as an escape hatch for constructs the interpreter can't handle natively. Enumerating all values of a type using fuel would work for finite types (bool, bounded int ranges) but not for unbounded ones (int, string). I could add a typeValues : LaurelType → Option (List LaurelValue) field to δ that returns some for enumerable types and none otherwise.

Happy to add this in a follow-up PR.

What does delegating to δ mean? Shouldn't these all return a not yet implemented error?

To implement old you'll need access to older versions of the heap, but it can be added later.

Yes, exactly. Implementing Old would require threading a "pre-state" snapshot through the interpreter, captured at procedure entry. Added a TODO for when we need postcondition evaluation.

The separation between LaurelConcreteEval, LaurelDenote and LaurelSemantics seems arbitrary to me.

LaurelSemantics defines shared types and helpers (values, stores, heaps, evalPrimOp). LaurelInterpreter (formerly LaurelDenote) is the fuel-based interpreter that uses those types. LaurelConcreteEval bridges the interpreter to Laurel.Program by building ProcEnv from program declarations and running main. The split keeps the interpreter independent of the program-level structure. Added module-level doc comments making this layering explicit.

Happy to merge some of these if you feel strongly about it.

This seems awfully complicated. Isn't the change on line 267 and 272 sufficient? If not, can you explain why?

Investigated. The simple change (just lines 267/272) handles the basic case where an imperative call's temp variable needs to be declared after its arguments' temps. But it does NOT handle the evaluation-order bug for side-effectful arguments like add({x:=1;x}, {x:=x+10;x}). In that case we need to:

1. Isolate each argument's prepended statements (so arg2's side effects don't leak into arg1's scope)
2. Capture side-effectful results in temporaries (so the final call uses snapshot values)
3. Emit the prepend groups in left-to-right order (so side effects execute in program order)

The simple fix only addresses point (1). Points (2) and (3) require the full complexity. Added a detailed comment in the code explaining which test cases require each piece.